文章背景与核心概要

本文介绍了 Baobab，这是一个创新的神经符号（NeSy）框架，旨在弥合深度学习与复杂 OWL 2 DL 本体之间的鸿沟。现有的神经符号方法通常通过将其限制在 Horn 片段（\(\mathcal{EL}^{++}\)）或放弃经典蕴涵来简化本体，而 Baobab 则支持在完整的 \(\mathcal{SROIQ}\) 描述逻辑上进行学习。

该框架通过基于后果的演算（consequence-based calculus）对命题核心进行饱和，并在活动域上实例化复杂特征（如名义值、数限制和角色公理），从而将 \(\mathcal{SROIQ}\) 本体编译为句决策图（SDDs）。利用条件证据的加权模型计数，该系统允许感知网络（如 CNN）在保持逻辑一致性的同时从部分监督中学习。作者证明了该方法有效地缓解了“推理捷径”（reasoning shortcuts），并实现了贝叶斯最优性能，且所有核心组件均在 Lean 4 中得到了机器验证。

摘要

Neuro-symbolic learning over OWL 2 DL via consequence-based compilation to differentiable circuits

Authors: Olga Mashkova, Asaad Mohammedsaleh, Fernando Zhapa-Camacho, Robert Hoehndorf
Published: August 18, 2026
Venue: Accepted at NeSy 2026
DOI: 10.48550/arXiv.2608.17741

---

Summary

This paper introduces Baobab, a novel neuro-symbolic (NeSy) framework designed to bridge the gap between deep learning and complex OWL 2 DL ontologies. While existing NeSy approaches often simplify ontologies by restricting them to the Horn fragment (\(\mathcal{EL}^{++}\)) or abandoning classical entailment, Baobab enables learning over the full \(\mathcal{SROIQ}\) description logic.

The framework functions by compiling \(\mathcal{SROIQ}\) ontologies into Sentential Decision Diagrams (SDDs). It achieves this by saturating a propositional core via a consequence-based calculus and instantiating complex features—such as nominals, number restrictions, and role axioms—over the active domain. By utilizing evidence-conditioned weighted model counting, the system allows perception networks (e.g., CNNs) to learn from partial supervision while maintaining logical consistency. The authors demonstrate that their approach effectively mitigates "reasoning shortcuts" and achieves Bayes-optimal performance, with all core components machine-checked in Lean 4.

核心贡献

Key Contributions

• Baobab Framework: A compilation-based approach that supports the full expressivity of \(\mathcal{SROIQ}\) ontologies.
• Mitigation of Reasoning Shortcuts: The first known method to characterize and address reasoning shortcuts in non-Horn description logics using a mixture model indexed by query justifications.
• Empirical Validation: Demonstrated on a real-image MNIST task, showing superior performance over standard single-WMC and learned ensemble methods.
• Formal Verification: The soundness of the compiler and the representation results are verified using the Lean 4 theorem prover.

• Baobab 框架： 一种基于编译的方法，支持 \(\mathcal{SROIQ}\) 本体完整的表达能力。
• 缓解推理捷径： 第一种已知的方法，通过使用以查询依据索引的混合模型，来表征和解决非 Horn 描述逻辑中的推理捷径。
• 实证验证： 在真实图像 MNIST 任务上进行验证，展示出优于标准单 WMC 和学习集成方法的性能。
• 形式化验证： 编译器的可靠性和表示结果已使用 Lean 4 定理证明器进行了验证。

访问与资源

Access & Resources

• Paper PDF: View on arXiv
• Source Code: GitHub Repository
• License: Creative Commons Attribution 4.0 International

• 论文 PDF： 在 arXiv 上查看
• 源代码： GitHub 仓库
• 许可证： 知识共享署名 4.0 国际许可协议

元数据

Metadata

Field	Details
arXiv ID	2608.17741
Primary Subject	Artificial Intelligence (cs.AI)
Submission Date	18 Aug 2026